
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">

<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<title>Module ErgoSpec.Translation.ErgoCompContext</title>
<meta name="description" content="Documentation of Coq module ErgoSpec.Translation.ErgoCompContext" />
<link href="coq2html.css" rel="stylesheet" type="text/css" />
<script type="text/javascript" src="coq2html.js"> </script>
</head>

<body onload="hideAll('proofscript')">
<h1 class="title">Module ErgoSpec.Translation.ErgoCompContext</h1>
<div class="coq">
<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html">String</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html">List</a></span>.<br/>
<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html">ErgoSpec.Backend.ErgoBackend</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html">ErgoSpec.Common.Utils.Result</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html">ErgoSpec.Common.Utils.Names</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html">ErgoSpec.Common.Utils.NamespaceContext</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html">ErgoSpec.Common.Types.ErgoType</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html">ErgoSpec.ErgoC.Lang.ErgoC</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCTypeContext.html">ErgoSpec.ErgoC.Lang.ErgoCTypeContext</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCStdlib.html">ErgoSpec.ErgoC.Lang.ErgoCStdlib</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html">ErgoSpec.Translation.ErgoNameResolve</a></span>.<br/>
<br/>
<span class="kwd">Section</span> <span class="id"><a name="ErgoCompContext">ErgoCompContext</a></span>.<br/>
&nbsp;&nbsp;<span class="kwd">Context</span> {<span class="id">bm</span> : <span class="id"><a href="https://querycert.github.io/html/Qcert.Common.TypeSystem.TBrandModel.html#brand_model">brand_model</a></span>}.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="function_group_env">function_group_env</a></span> : <span class="kwd">Set</span> := <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_function">ergoc_function</a></span>)).<br/>
&nbsp;&nbsp;<br/>
&nbsp;&nbsp;<span class="kwd">Record</span> <span class="id"><a name="compilation_context">compilation_context</a></span> : <span class="kwd">Set</span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a name="mkCompCtxt">mkCompCtxt</a></span> {<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a name="compilation_context_namespace">compilation_context_namespace</a></span>: <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span>;                     <span class="docright">(* for name resolution  *)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a name="compilation_context_function_env">compilation_context_function_env</a></span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_function">ergoc_function</a></span>); <span class="docright">(* functions in scope  *)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a name="compilation_context_function_group_env">compilation_context_function_group_env</a></span> : <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#function_group_env">function_group_env</a></span>;       <span class="docright">(* functions groups in scope  *)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a name="compilation_context_global_env">compilation_context_global_env</a></span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_expr">ergoc_expr</a></span>);       <span class="docright">(* global variables in scope  *)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a name="compilation_context_local_env">compilation_context_local_env</a></span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_expr">ergoc_expr</a></span>);        <span class="docright">(* local variables in scope  *)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a name="compilation_context_params_env">compilation_context_params_env</a></span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>;                      <span class="docright">(* function parameters in scope  *)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a name="compilation_context_current_contract">compilation_context_current_contract</a></span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#option">option</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>;              <span class="docright">(* current contract in scope if any  *)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a name="compilation_context_current_clause">compilation_context_current_clause</a></span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#option">option</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>;                <span class="docright">(* current clause in scope if any  *)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a name="compilation_context_type_ctxt">compilation_context_type_ctxt</a></span> : <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCTypeContext.html#type_context">type_context</a></span>;                      <span class="docright">(* the type context  *)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a name="compilation_context_type_decls">compilation_context_type_decls</a></span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#laergo_type_declaration">laergo_type_declaration</a></span>;     <span class="docright">(* type declarations  *)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a name="compilation_context_new_type_decls">compilation_context_new_type_decls</a></span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#laergo_type_declaration">laergo_type_declaration</a></span>; <span class="docright">(* type declarations  *)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;}.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="namespace_ctxt_of_compilation_context">namespace_ctxt_of_compilation_context</a></span> (<span class="id">ctxt</span>:<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span>) : <span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_namespace">compilation_context_namespace</a></span>).<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="compilation_context_update_namespace">compilation_context_update_namespace</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ctxt</span>:<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span>) (<span class="id">nsctxt</span>:<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt">namespace_ctxt</a></span>) : <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#mkCompCtxt">mkCompCtxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#nsctxt">nsctxt</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_function_env">compilation_context_function_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_function_group_env">compilation_context_function_group_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_global_env">compilation_context_global_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_local_env">compilation_context_local_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_params_env">compilation_context_params_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_current_contract">compilation_context_current_contract</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_current_clause">compilation_context_current_clause</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_type_ctxt">compilation_context_type_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_type_decls">compilation_context_type_decls</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_new_type_decls">compilation_context_new_type_decls</a></span>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="compilation_context_update_function_env">compilation_context_update_function_env</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ctxt</span> : <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">name</span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">value</span> : <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_function">ergoc_function</a></span>) : <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#mkCompCtxt">mkCompCtxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_namespace">compilation_context_namespace</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;((<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#name">name</a></span>, <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#value">value</a></span>)::<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_function_env">compilation_context_function_env</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_function_group_env">compilation_context_function_group_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_global_env">compilation_context_global_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_local_env">compilation_context_local_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_params_env">compilation_context_params_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_current_contract">compilation_context_current_contract</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_current_clause">compilation_context_current_clause</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_type_ctxt">compilation_context_type_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_type_decls">compilation_context_type_decls</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_new_type_decls">compilation_context_new_type_decls</a></span>).<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="update_function_group_env">update_function_group_env</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">gname</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">fname</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">fn</span>:<span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_function">ergoc_function</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">fg_env</span>:<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#function_group_env">function_group_env</a></span>) : <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#function_group_env">function_group_env</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Assoc.html#lookup">lookup</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string_dec">string_dec</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#fg_env">fg_env</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#gname">gname</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">t</span> =&gt; <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Assoc.html#update_first">update_first</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string_dec">string_dec</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#fg_env">fg_env</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#gname">gname</a></span> ((<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#fname">fname</a></span>,<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#fn">fn</a></span>)::<span class="id">t</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt; (<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#gname">gname</a></span>,((<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#fname">fname</a></span>,<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#fn">fn</a></span>)::<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>)) :: <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#fg_env">fg_env</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="compilation_context_update_function_group_env">compilation_context_update_function_group_env</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ctxt</span> : <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">coname</span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">clname</span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">value</span> : <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_function">ergoc_function</a></span>) : <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#mkCompCtxt">mkCompCtxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_namespace">compilation_context_namespace</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_function_env">compilation_context_function_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#update_function_group_env">update_function_group_env</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#coname">coname</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#clname">clname</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#value">value</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_function_group_env">compilation_context_function_group_env</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_global_env">compilation_context_global_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_local_env">compilation_context_local_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_params_env">compilation_context_params_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_current_contract">compilation_context_current_contract</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_current_clause">compilation_context_current_clause</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_type_ctxt">compilation_context_type_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_type_decls">compilation_context_type_decls</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_new_type_decls">compilation_context_new_type_decls</a></span>).<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="compilation_context_update_global_env">compilation_context_update_global_env</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ctxt</span> : <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">name</span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">value</span> : <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_expr">ergoc_expr</a></span>) : <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#mkCompCtxt">mkCompCtxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_namespace">compilation_context_namespace</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_function_env">compilation_context_function_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_function_group_env">compilation_context_function_group_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;((<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#name">name</a></span>, <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#value">value</a></span>)::<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_global_env">compilation_context_global_env</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_local_env">compilation_context_local_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_params_env">compilation_context_params_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_current_contract">compilation_context_current_contract</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_current_clause">compilation_context_current_clause</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_type_ctxt">compilation_context_type_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_type_decls">compilation_context_type_decls</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_new_type_decls">compilation_context_new_type_decls</a></span>).<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="compilation_context_update_local_env">compilation_context_update_local_env</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ctxt</span> : <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">name</span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">value</span> : <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_expr">ergoc_expr</a></span>) : <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#mkCompCtxt">mkCompCtxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_namespace">compilation_context_namespace</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_function_env">compilation_context_function_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_function_group_env">compilation_context_function_group_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_global_env">compilation_context_global_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;((<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#name">name</a></span>, <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#value">value</a></span>)::<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_local_env">compilation_context_local_env</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_params_env">compilation_context_params_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_current_contract">compilation_context_current_contract</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_current_clause">compilation_context_current_clause</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_type_ctxt">compilation_context_type_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_type_decls">compilation_context_type_decls</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_new_type_decls">compilation_context_new_type_decls</a></span>).<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="compilation_context_set_local_env">compilation_context_set_local_env</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ctxt</span> : <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">new_local_env</span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoC.html#ergoc_expr">ergoc_expr</a></span>)) : <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#mkCompCtxt">mkCompCtxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_namespace">compilation_context_namespace</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_function_env">compilation_context_function_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_function_group_env">compilation_context_function_group_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_global_env">compilation_context_global_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#new_local_env">new_local_env</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_params_env">compilation_context_params_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_current_contract">compilation_context_current_contract</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_current_clause">compilation_context_current_clause</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_type_ctxt">compilation_context_type_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_type_decls">compilation_context_type_decls</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_new_type_decls">compilation_context_new_type_decls</a></span>).<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="compilation_context_update_params_env">compilation_context_update_params_env</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ctxt</span> : <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">param</span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) : <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#mkCompCtxt">mkCompCtxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_namespace">compilation_context_namespace</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_function_env">compilation_context_function_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_function_group_env">compilation_context_function_group_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_global_env">compilation_context_global_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_local_env">compilation_context_local_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#param">param</a></span>::<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_params_env">compilation_context_params_env</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_current_contract">compilation_context_current_contract</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_current_clause">compilation_context_current_clause</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_type_ctxt">compilation_context_type_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_type_decls">compilation_context_type_decls</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_new_type_decls">compilation_context_new_type_decls</a></span>).<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="compilation_context_set_params_env">compilation_context_set_params_env</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ctxt</span> : <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">params</span> : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) : <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#mkCompCtxt">mkCompCtxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_namespace">compilation_context_namespace</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_function_env">compilation_context_function_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_function_group_env">compilation_context_function_group_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_global_env">compilation_context_global_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_local_env">compilation_context_local_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#params">params</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_current_contract">compilation_context_current_contract</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_current_clause">compilation_context_current_clause</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_type_ctxt">compilation_context_type_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_type_decls">compilation_context_type_decls</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_new_type_decls">compilation_context_new_type_decls</a></span>).<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="set_namespace_in_compilation_context">set_namespace_in_compilation_context</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ns</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Names.html#namespace_name">namespace_name</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ctxt</span>:<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;: <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#elift">elift</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_update_namespace">compilation_context_update_namespace</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoNameResolve.html#new_ergo_module_namespace">new_ergo_module_namespace</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#namespace_ctxt_of_compilation_context">namespace_ctxt_of_compilation_context</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ns">ns</a></span>).<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="set_current_contract">set_current_contract</a></span> (<span class="id">ctxt</span>:<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span>) (<span class="id">cname</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) : <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#mkCompCtxt">mkCompCtxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_namespace">compilation_context_namespace</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_function_env">compilation_context_function_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_function_group_env">compilation_context_function_group_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_global_env">compilation_context_global_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_local_env">compilation_context_local_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_params_env">compilation_context_params_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#cname">cname</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_current_clause">compilation_context_current_clause</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_type_ctxt">compilation_context_type_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_type_decls">compilation_context_type_decls</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_new_type_decls">compilation_context_new_type_decls</a></span>).<br/>
&nbsp;&nbsp;<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="set_current_clause">set_current_clause</a></span> (<span class="id">ctxt</span>:<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span>) (<span class="id">cname</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) : <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#mkCompCtxt">mkCompCtxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_namespace">compilation_context_namespace</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_function_env">compilation_context_function_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_function_group_env">compilation_context_function_group_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_global_env">compilation_context_global_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_local_env">compilation_context_local_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_params_env">compilation_context_params_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_current_contract">compilation_context_current_contract</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#cname">cname</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_type_ctxt">compilation_context_type_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_type_decls">compilation_context_type_decls</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_new_type_decls">compilation_context_new_type_decls</a></span>).<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="compilation_context_update_type_ctxt">compilation_context_update_type_ctxt</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ctxt</span>: <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">nctxt</span>: <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCTypeContext.html#type_context">type_context</a></span>) : <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#mkCompCtxt">mkCompCtxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_namespace">compilation_context_namespace</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_function_env">compilation_context_function_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_function_group_env">compilation_context_function_group_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_global_env">compilation_context_global_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_local_env">compilation_context_local_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_params_env">compilation_context_params_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_current_contract">compilation_context_current_contract</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_current_clause">compilation_context_current_clause</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#nctxt">nctxt</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_type_decls">compilation_context_type_decls</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_new_type_decls">compilation_context_new_type_decls</a></span>).<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="compilation_context_update_type_declarations">compilation_context_update_type_declarations</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ctxt</span>: <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">old_decls</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#laergo_type_declaration">laergo_type_declaration</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">new_decls</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#laergo_type_declaration">laergo_type_declaration</a></span>)  : <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#mkCompCtxt">mkCompCtxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_namespace">compilation_context_namespace</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_function_env">compilation_context_function_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_function_group_env">compilation_context_function_group_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_global_env">compilation_context_global_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_local_env">compilation_context_local_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_params_env">compilation_context_params_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_current_contract">compilation_context_current_contract</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_current_clause">compilation_context_current_clause</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_type_ctxt">compilation_context_type_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#old_decls">old_decls</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#new_decls">new_decls</a></span>.<br/>
&nbsp;&nbsp;<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="compilation_context_add_new_type_declaration">compilation_context_add_new_type_declaration</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ctxt</span>: <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">decl</span>:<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#laergo_type_declaration">laergo_type_declaration</a></span>) : <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#mkCompCtxt">mkCompCtxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_namespace">compilation_context_namespace</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_function_env">compilation_context_function_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_function_group_env">compilation_context_function_group_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_global_env">compilation_context_global_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_local_env">compilation_context_local_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_params_env">compilation_context_params_env</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_current_contract">compilation_context_current_contract</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_current_clause">compilation_context_current_clause</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_type_ctxt">compilation_context_type_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_type_decls">compilation_context_type_decls</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_new_type_decls">compilation_context_new_type_decls</a></span>) ++ (<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#decl">decl</a></span>::<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>)).<br/>
&nbsp;&nbsp;<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="init_compilation_context">init_compilation_context</a></span> <span class="id">nsctxt</span> : <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#mkCompCtxt">mkCompCtxt</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#nsctxt">nsctxt</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> <span class="id"><a href="ErgoSpec.ErgoC.Lang.ErgoCTypeContext.html#empty_type_context">ErgoCTypeContext.empty_type_context</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="is_abstract_class">is_abstract_class</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ctxt</span>: <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context">compilation_context</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">n</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">if</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#in_dec">in_dec</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string_dec">string_dec</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#n">n</a></span> <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ctxt">ctxt</a></span>.(<span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#compilation_context_namespace">compilation_context_namespace</a></span>).(<span class="id"><a href="ErgoSpec.Common.Utils.NamespaceContext.html#namespace_ctxt_abstract">namespace_ctxt_abstract</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">then</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#true">true</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">else</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#false">false</a></span>.<br/>
&nbsp;&nbsp;<br/>
<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.Translation.ErgoCompContext.html#ErgoCompContext">ErgoCompContext</a></span>.<br/>

</div>
<div class="footer"><hr/>Generated by <a href="https://github.com/xavierleroy/coq2html/">coq2html</div>
</body>
</html>
